\begin{tabbing}
es{-}first{-}at{-}since(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=loc($e$) $=$ $i$\+
\\[0ex]\& $P$($e$) \& $\neg$$R$($e$)
\\[0ex]\& ($\forall$${\it e'}$$<$$e$. $P$(${\it e'}$) $\Rightarrow$ ($\exists$${\it e''}$:E. ${\it e'}$ $\leq$ ${\it e''}$  \& (${\it e''}$ $<$loc $e$) \& $R$(${\it e''}$)))
\-
\end{tabbing}